the_es:ES, e:E, l:IdLnk, m:Msg.
(m  sends(l;e))
 e':rvc(l,mtag(m),v).(e < e') & msgtype(m) = valtype(e')  Type & v = mval(m)  valtype(e') 

latex

Definitions	t  T, P  Q, x:A. B(x), P & Q, A & B, mval(m), val(e), valtype(e), msgtype(m), (e < e'), mtag(m), tag(e), Id, lnk(e), IdLnk, isrcv(e), b, Prop, x:A. B(x), e:rvc(l,tg,v).P(e;v), AB, i  j < k, {i..j}, ||as||, False, A, , E, (Msg on l), Msg, S  T, sends(l;e), l[i], (x  l), ES, msg(l;t;v), index(e), True, T, SQType(T), Msg(M)
Lemmas	es-sender-causl, es-mval-valtype, squash wf, true wf, event system wf, es-axioms, nat wf, length wf1, es-Msgl wf, select wf, es-sends wf, es-Msg wf, IdLnk wf, es-E wf, le wf, assert wf, es-isrcv wf, es-lnk wf, Id wf, es-tag wf, es-mtag wf, es-causl wf, es-msgtype wf, es-valtype wf, es-val wf, es-mval wf